A:Type. (x, y:A. Dec(x = y))  (L1, L2:(A List). Dec(l_disjoint(A;L1;L2))) 

latex

Definitions	t  T, type List, x:A. B(x), x:AB(x), l_disjoint(T;l1;l2), Dec(P), s = t, , P  Q, Type, [], A, P  Q, left + right, #$n, ||as||, a < b, Void, False, A  B, , {x:A| B(x)} , , l[i], A c B, x:A  B(x), (x  l), P & Q, P  Q, [car / cdr], as @ bs, s ~ t, x:A.B(x), P  Q
Lemmas	l disjoint append2, append wf, decidable functionality, and functionality wrt iff, l disjoint singleton2, decidable cand, decidable not, decidable l member, l member wf, nil member, length wf2, nat wf, length wf1, select wf, not wf, l disjoint wf, decidable wf